(** 
    The dynamic interpreter for the Gnarly Programming Language. The contents of this file are designed to evaluate the the abstract syntax tree of 
    a Gnarly program, so many of the constructs of {i gnexp} have their own evaluating functions.
    @author mmvitousek
*)

open Gnsyn
open Printing
open Sinterp
open List
exception TooManyArgs
exception TooFewArgs
exception DynamicTypeException of gnvalue

(** 
    Main entry point for dynamic interpreter. 
    @param program a {i gnarly} expression to be interpreted
    @param environment the current execution environment
    @return a value of {i gnvalue}
*)
let rec gnarly_interpret program environment = 
	match program with
		  Empty 		-> N
		| Expression(expr)	-> eval_expr environment expr
		| Library(stng)		-> N 
		| Syntax_Error          -> N
(** 
    Evaluator for individual expression of type {i gnexp}. Either reduces to a {i gnvalue} in one step, or calls another function to perform additional steps.
    @param env the current execution environment
    @param exp the {i gnexp} expression to be evaluated
    @return a {i gnvalue} that {b exp} reduces to in one or more steps*)
and eval_expr env exp =
	match exp with
		  Real(number)			-> R(number)
		| Integer(number)		-> I(IVal(number))
		| Boolean(boole)		-> B(boole)
		| Char(chr)			-> Ch(chr)
		| Nil				-> N
		| Identifier(strng)		-> lookup env strng
		| Lambda(varlist, typ, expr)	-> eval_closure env varlist typ expr exp
		| Application(funexpr, args)	-> eval_application env funexpr args exp
		| Let(terms, rest)	        -> eval_let env terms rest exp
		| Commit(terms)	         	-> eval_commit env terms exp
		| Sequence(expr1,expr2)		-> eval_seq env expr1 expr2 exp
		| Conditional(cond, truthbranch, falsebranch,_)
			-> eval_cond env cond truthbranch falsebranch exp
		| Match(targ, cases, def, _)		-> eval_match env targ cases def exp
(** 
    Matches {i gnvalue}s and {i gntype}s to perform runtime type checking
    @param typ the {i gntype} to be matched against
    @param vl the {i gnvalue} being typechecked
    @return {e true} if the typechecking succeeds, or {e false} if it fails
*)
and match_types_vals typ vl =
	match typ, vl with
		  Dynamic_Type, _                  -> true
		| Type_Variable(_), _              -> true
		| Exclusive_Type_Variable(_,n), _  -> true
		| Basic_Type("Int"), I(_)          -> true
		| Basic_Type("Boolean"), B(_)      -> true
		| Basic_Type("Real"), R(_)         -> true
		| Basic_Type("Char"), Ch(_)        -> true
		| Basic_Type("Nil"), N             -> true
		| Product_Type(pa::[]), _          -> match_types_vals pa vl
		| Product_Type(pa::pas), C(a,b)    -> (match_types_vals pa a) && (match_types_vals (Product_Type(pas)) b)
		| List_Type(_), N                  -> true
		| List_Type(List(pa)), C(a,b)      -> (match_types_vals pa a) && (match_types_vals (List_Type(List(pa))) b)
		| Arrow_Type(_,_), F(_,ftyp,_,_)   -> match_types typ ftyp
		| Arrow_Type(_,_), PF(_)           -> true
		| _, _                             -> false
(** 
    Typechecks lists of {i gnvalue}s and {i gntype}s, using {b match_types_vals}.
    @param types the {i gntype}s to be matched against
    @param vals the {i gnvalue}s being typechecked
    @return {e true} if the typechecking succeeds, or {e false} if it fails or if the parameters are not equal in length
*)
and match_tvlist types vals = try (fold_left (&&) true (map2 match_types_vals types vals)) with Invalid_argument(_) -> false
(** 
    Extends the execution environment with a new identifier and value pair.
    @param env the current execution environment
    @param k a {i string} containing the name of the new identifier
    @param v a {i gnvalue} containing the value of the new identifier
    @return an extended execution environment including the new pair
*)
and extend_env env k v = 
	match (!env) with
		  Env(en) -> ref (Env((k, (ref v))::(en)))
		  
and multi_extend_env env ks vs = 
	match ks, vs with
		  kk::kks, vv::vvs	-> multi_extend_env (extend_env env kk vv) kks vvs
		| [], []		-> env
		| _, _			-> raise ListLengthMismatch
(**
   Retrieves the value of an identifier from the execution environment.
   @param env the current execution environment
   @param x a {i string} containing the name of the identifier whose value is being looked up
   @return a {i gnvalue} corresponding to the identifier specified by {b x}
*)
and lookup env x = 
	match (!env) with Env(en) -> (try !(assoc x en) with Not_found -> Type_Error("Undefined identifier " ^ x))
(**
   Evaluates the contents of a {e Lambda} term by reifying the current execution environment along with the closure's type, variable list, and body.
   @param env the current execution environment
   @param varlist a list of {i string}s naming the variables used as parameters to the closure
   @param typ the explicit type of the closure
   @param expr the body of the closure
   @param cexp the {i gnexp} being evaluated
   @return a {e F} {i gnvalue} representing the created closure
*)
and eval_closure env varlist typ expr cexp = 
	F(varlist, typ, expr, (ref env))
(**
   Evaluates the contents of a {e Application} term by extending the reified environment of the applied function with the values given as parameters.
   @param env the current execution environment
   @param func a {i gnexp}, expected to evaluate to a {e F} or {e PF}, to be applied to the parameters in {b args}
   @param args a list of {i gnexp}s to be evaluated and then passed to {b func} as parameters
   @param cexp the {i gnexp} being evaluated
   @return a {i gnvalue} representing the result of the function application
*)
and eval_application env func args cexp = 
    let eval_args oenv vals = map (eval_expr oenv) vals (* takes a list of gnexps and evaluates each in turn *)
	in let rec extend_args env names vals = (* extends the local environment with the evaluated parameters *)
		match names, vals with  
			  x::xs, expr::exprs -> extend_args (extend_env env x expr) xs exprs 
			| [], []             -> env
			| [], _              -> raise (DynamicTypeException (Type_Error("Too few arguments provided to function application" 
											^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))))
			| _, []              -> raise (DynamicTypeException (Type_Error("Too many arguments provided to function application" 
											^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))))
	and clarify evars ert = (* raise an error if any of the evaluated parameters are in error *)
		match evars, ert with
			  _, Type_Error(_)     -> raise (DynamicTypeException ert)
			| Type_Error(x)::vs,_  -> raise (DynamicTypeException (Type_Error(x)))
			| v::vs,_              -> clarify vs ert
			| [],_                 -> ()
	in let efun = eval_expr env func 
	in match efun with
		  F(varlist, typ, expr, lenv)	-> 
			  let evars = eval_args env args
			  in (try (let ert = eval_expr (extend_args !lenv varlist evars) expr (* evaluate the body of the function using the function's local
												  environment, extended to include the evaluated parameters *)
				   in clarify evars ert; 
					   match typ with
						     Arrow_Type(vt, rt)   -> 
							     if not (match_tvlist vt evars) then 
								     Type_Error("Function application expects arguments of types " 
										^ (string_of_typelist vt) ^ ", given " ^ (string_of_vallist evars) 
										^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp))
							     else if not (match_types_vals rt ert) then
								     Type_Error("Function application expects result of type " 
										^ (string_of_gntype rt) ^ ", given " ^ (string_of_gnvalue ert) 
										^ "\n\t\tIn expression: " ^ (string_of_gnexp cexp))
							     else ert
						   | Dynamic_Type         -> ert
						   | _                    -> Type_Error("Applied term has type " ^ (string_of_gntype typ) 
											^ ", expected Dynamic or X -> X type\n\t\tIn expression: " 
											^ (string_of_gnexp cexp))
				  ) with DynamicTypeException(ex) -> ex 
			     )				     
		| PF(func)			-> (try (func env args cexp) with 
							      TooManyArgs   -> Type_Error("Too many arguments provided to function application" 
											  ^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))
							    | TooFewArgs    -> Type_Error("Too few arguments provided to function application" 
											  ^ " \n\t\tIn expression: " ^ (string_of_gnexp cexp))
						   )
		| Type_Error(_)			-> efun
		| _ 				-> Type_Error("Applied term has form " ^ (string_of_gnvalue efun) 
							      ^ ", expected term of type Dynamic or X -> X type \n\t\tIn expression: " ^ (string_of_gnexp cexp))
(**
   Evaluates the contents of a {e Let} term by extending the execution environment with a key/value pair representing a new identifier, before executing the 
   remaining body of the term. If the value of the new identifier is a {e F} closure, then its local environment is also extended to include the identifier.
   @param env the current execution environment
   @param identifier a {i string} consisting of the name of the new identifier
   @param typ a {i gntype} indicating the expected type of the identifier
   @param value a {i gnexp} to be evaluated and then assigned as the value of {b identifier}
   @param rest the term to be evaluated within the extended environment
   @param cexp the {i gnexp} being evaluated
   @return the result of evaluating {b rest} within the extended environment
*)
and eval_let env terms rest cexp =
	let eval_term id typ value = 
		let eval = eval_expr env value 
		in if not (match_types_vals typ eval)
			then raise (DynamicTypeException (Type_Error("Term assigned to " ^ id ^ " has value " ^ (string_of_gnvalue eval) 
								     ^ ", expected term of type " ^ (string_of_gntype typ) ^ "\n\t\tIn expression: " 
								     ^ (string_of_gnexp cexp))))
			else match eval with 
				  F(_, _, _, lenv)	-> lenv := (extend_env !lenv id eval); (id, eval)
				| _			-> (id, eval)
	in let eval_terms terms = map (fun ((id, typ), value) -> eval_term id typ value) terms
	and extend_env_list env pairs = 
		let kk, vv = split pairs
		in multi_extend_env env kk vv
	in let rec fix_terms pairs refer = 
			let remove_self id pairs = remove_assoc id pairs
			in match pairs with 
				  (id, F(_,_,_,lenv))::ps -> lenv := (extend_env_list !lenv (remove_self id refer));
					  fix_terms ps refer
				| pair::ps                -> fix_terms ps refer
				| []                      -> ()
	in try (
		let eterms = eval_terms terms 
		in fix_terms eterms eterms;
		eval_expr (extend_env_list env eterms) rest
	) with DynamicTypeException(ex) -> ex
(**
   Evaluates the contents of a {e Commit} term by extending and mutating the execution environment with a key/value pair representing a new identifier. 
   If the value of the new identifier is a {e F} closure, then its local environment is also extended to include the identifier.
   @param env the current execution environment
   @param identifier a {i string} consisting of the name of the new identifier
   @param typ a {i gntype} indicating the expected type of the identifier
   @param value a {i gnexp} to be evaluated and then assigned as the value of {b identifier}
   @param cexp the {i gnexp} being evaluated
   @return a {i gnvalue} representing a statement that {b identifier} has been defined.
*)
and eval_commit env terms cexp =
	let eval_term id typ value = 
		let eval = eval_expr env value 
		in if not (match_types_vals typ eval)
			then raise (DynamicTypeException (Type_Error("Term assigned to " ^ id ^ " has value " ^ (string_of_gnvalue eval) 
								     ^ ", expected term of type " ^ (string_of_gntype typ) ^ "\n\t\tIn expression: " 
								     ^ (string_of_gnexp cexp))))
			else match eval with 
				  F(varlist, _, lexpr, lenv)	-> lenv := (extend_env !lenv id eval);
					  (id, eval)
				| _				-> (id, eval)
	in let eval_terms terms = map (fun ((id, typ), value) -> eval_term id typ value) terms
	and extend_env_list env pairs = 
            let kk, vv = split pairs 
	    in multi_extend_env env kk vv
	in let rec fix_terms pairs refer = 
			let remove_self id pairs = remove_assoc id pairs
			in match pairs with 
				  (id, F(_,_,_,lenv))::ps -> lenv := (extend_env_list !lenv (remove_self id refer));
					  fix_terms ps refer
				| pair::ps                -> fix_terms ps refer
				| []                      -> ()
	in try (
		let eterms = eval_terms terms 
		in fix_terms eterms eterms;
		env := !(extend_env_list env eterms);
		N
		) with DynamicTypeException(ex) -> ex
(**
   Evaluates the contents of a {e Sequence} term by evaluating the first part of the sequence, so that any side effects contained therein can occur, and then
   returning the evaluated second part of the sequence.
   @param env the current execution environment
   @param expr1 the first {i gnexp} to be evaluated
   @param expr2 the second {i gnexp} to be evaluated
   @param cexp the {i gnexp} being evaluated
   @return a {i gnvalue} obtained by evaluation of {b expr2}
*)
and eval_seq env expr1 expr2 cexp =
	eval_expr env expr1;
	eval_expr env expr2
(**
   Evaluates the contents of a {e Conditional} term by evaluating the branching term, and then evaluating and returning either the true branch or false branch 
   depending on the value of the branching term.
   @param env the current execution environment
   @param cond the branching term
   @param truthbranch the term to be evaluated and returned if {b cond} evaluates to {e B(true)}
   @param falsebranch the term to be evaluated and returned if {b cond} evaluates to {e B(false)}
   @param cexp the {i gnexp} being evaluated
   @return the evaluation of either {b truthbranch} or {b falsebranch}
*)
and eval_cond env cond truthbranch falsebranch cexp =
	let eoper = eval_expr env cond in
		match eoper with
			  B(boole)	-> if boole then eval_expr env truthbranch else eval_expr env falsebranch
			| Type_Error(_)	-> eoper
			| _ 		-> Type_Error("Branching term of conditional has form " ^ (string_of_gnvalue eoper) 
						      ^ ", expected term of type Boolean\n\t\tIn expression: " ^ (string_of_gnexp cexp))
(**
   Evaluates the contents of a {e Match} term by evaluating the target term and matching it against head::tail patterns until a match is found, at which
   point the corresponding term is executed. If no match is found, the default term is executed
   @param env the current execution environment
   @param target the {i gnexp} to be evaluated and then matched against
   @param cases a list of pairs consisting of a list of {i string}s, defining a match pattern, and a {i gnexp}
   @param default a {i gnexp} to be executed if none of the patterns match the target
   @param cexp the {i gnexp} being evaluated
   @return the evaluation of the first term within {b cases} whose mattern matched {b target} successfully, or the evaluation of {b default} if no patterns match
*)
and eval_match env target cases default cexp =
	let rec case_match env cases etarg default = 
		match cases with 
			  (terms, exp)::cs	-> if match_terms terms etarg then eval_expr (extend_terms env terms etarg) exp else case_match env cs etarg default
			| []			-> eval_expr env default
        and match_terms terms etarg =
                match terms, etarg with         
                          "NIL"::[], N                -> true
                        | x::[], C(ca, cd)        -> x <> "NIL"
                        | x::[], N                -> true
                        | x::xs, C(ca, cd)        -> match_terms xs cd
                        | _, _                        -> false
        and extend_terms env terms etarg =
                match terms, etarg with         
                          "NIL"::[], N                -> env
                        | x::[], C(ca, cd)        -> extend_env env x etarg
                        | x::[], N                -> extend_env env x etarg
                        | x::xs, C(ca, cd)        -> extend_terms (extend_env env x ca) xs cd
                        | _, _                        -> env
        in let etarg = eval_expr env target 
        in case_match env cases etarg default
(** Converts a {i string} to a {i gnvalue} *)
and make_gnstring strng =
        match strng with
                  ""        -> N
                | _        -> C(Ch(strng.[0]), (make_gnstring (String.sub strng 1 ((String.length strng) - 1))))
